Nuprl Lemma : prod_sum_r_q
11,40
postcript
pdf
a
,
b
:
. (
a
b
)
(
E
:({
a
..
b
}
),
u
:
. (
a
j
<
b
.
E
(
j
) *
u
) =
a
j
<
b
.
E
(
j
) *
u
)
latex
Definitions
t
T
,
t
.2
,
t
.1
,
CRng
,
<
+*>
,
*
,
x
f
y
,
|
r
|
,
x
:
A
.
B
(
x
)
,
a
j
<
b
.
E
(
j
)
Lemmas
crng
wf
,
qrng
wf
,
rng
times
sum
r
origin
a, b:
. (a 
b) 
(E:({a..b
}
), u:. (
a j < b. E(j) * u) = a j < b. E(j) * u 
) a, b:. (a b) (E:({a..b}), u:. (a j < b. E(j) * u) = a j < b. E(j) * u ) T+*>x:A. B(x)a j < b. E(j)